\begin{tabbing}
$\forall$\=$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$),\+
\\[0ex]$P$:($x$:\{$x$:$A$$\mid$ $x$ $\in$ dom($f$) \}$\rightarrow$$B$($x$)$\rightarrow$Prop).
\-\\[0ex]$\forall$$x$$\in$dom($f$). $v$=$f$($x$) $\Rightarrow$  $P$($x$,$v$) $\in$ Prop
\end{tabbing}